Termination w.r.t. Q proof of /tmp/tmpc-MbFs/cime3.trs

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

a__a → a__c
a__b → a__c
a__c → e
a__k → l
a__d → m
a__a → a__d
a__b → a__d
a__c → l
a__k → m
a__A → a__h(a__f(a__a), a__f(a__b))
a__h(X, X) → a__g(mark(X), mark(X), a__f(a__k))
a__g(d, X, X) → a__A
a__f(X) → a__z(mark(X), X)
a__z(e, X) → mark(X)
mark(A) → a__A
mark(a) → a__a
mark(b) → a__b
mark(c) → a__c
mark(d) → a__d
mark(k) → a__k
mark(z(X1, X2)) → a__z(mark(X1), X2)
mark(f(X)) → a__f(mark(X))
mark(h(X1, X2)) → a__h(mark(X1), mark(X2))
mark(g(X1, X2, X3)) → a__g(mark(X1), mark(X2), mark(X3))
mark(e) → e
mark(l) → l
mark(m) → m
a__A → A
a__a → a
a__b → b
a__c → c
a__d → d
a__k → k
a__z(X1, X2) → z(X1, X2)
a__f(X) → f(X)
a__h(X1, X2) → h(X1, X2)
a__g(X1, X2, X3) → g(X1, X2, X3)

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

a__a → a__c
a__b → a__c
a__c → e
a__k → l
a__d → m
a__a → a__d
a__b → a__d
a__c → l
a__k → m
a__A → a__h(a__f(a__a), a__f(a__b))
a__h(X, X) → a__g(mark(X), mark(X), a__f(a__k))
a__g(d, X, X) → a__A
a__f(X) → a__z(mark(X), X)
a__z(e, X) → mark(X)
mark(A) → a__A
mark(a) → a__a
mark(b) → a__b
mark(c) → a__c
mark(d) → a__d
mark(k) → a__k
mark(z(X1, X2)) → a__z(mark(X1), X2)
mark(f(X)) → a__f(mark(X))
mark(h(X1, X2)) → a__h(mark(X1), mark(X2))
mark(g(X1, X2, X3)) → a__g(mark(X1), mark(X2), mark(X3))
mark(e) → e
mark(l) → l
mark(m) → m
a__A → A
a__a → a
a__b → b
a__c → c
a__d → d
a__k → k
a__z(X1, X2) → z(X1, X2)
a__f(X) → f(X)
a__h(X1, X2) → h(X1, X2)
a__g(X1, X2, X3) → g(X1, X2, X3)

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

MARK(g(X1, X2, X3)) → MARK(X2)
MARK(b) → A__B
A__A¹ → A__A
MARK(k) → A__K
A__A¹ → A__H(a__f(a__a), a__f(a__b))
MARK(g(X1, X2, X3)) → A__G(mark(X1), mark(X2), mark(X3))
A__H(X, X) → MARK(X)
A__F(X) → MARK(X)
A__G(d, X, X) → A__A¹
A__A¹ → A__B
A__A → A__C
A__A → A__D
MARK(A) → A__A¹
A__H(X, X) → A__K
A__A¹ → A__F(a__b)
A__A¹ → A__F(a__a)
MARK(z(X1, X2)) → MARK(X1)
MARK(f(X)) → MARK(X)
MARK(g(X1, X2, X3)) → MARK(X1)
A__F(X) → A__Z(mark(X), X)
MARK(h(X1, X2)) → A__H(mark(X1), mark(X2))
MARK(h(X1, X2)) → MARK(X1)
A__B → A__C
A__H(X, X) → A__G(mark(X), mark(X), a__f(a__k))
A__H(X, X) → A__F(a__k)
A__Z(e, X) → MARK(X)
MARK(z(X1, X2)) → A__Z(mark(X1), X2)
MARK(g(X1, X2, X3)) → MARK(X3)
MARK(h(X1, X2)) → MARK(X2)
MARK(a) → A__A
MARK(c) → A__C
MARK(f(X)) → A__F(mark(X))
MARK(d) → A__D
A__B → A__D

The TRS R consists of the following rules:

a__a → a__c
a__b → a__c
a__c → e
a__k → l
a__d → m
a__a → a__d
a__b → a__d
a__c → l
a__k → m
a__A → a__h(a__f(a__a), a__f(a__b))
a__h(X, X) → a__g(mark(X), mark(X), a__f(a__k))
a__g(d, X, X) → a__A
a__f(X) → a__z(mark(X), X)
a__z(e, X) → mark(X)
mark(A) → a__A
mark(a) → a__a
mark(b) → a__b
mark(c) → a__c
mark(d) → a__d
mark(k) → a__k
mark(z(X1, X2)) → a__z(mark(X1), X2)
mark(f(X)) → a__f(mark(X))
mark(h(X1, X2)) → a__h(mark(X1), mark(X2))
mark(g(X1, X2, X3)) → a__g(mark(X1), mark(X2), mark(X3))
mark(e) → e
mark(l) → l
mark(m) → m
a__A → A
a__a → a
a__b → b
a__c → c
a__d → d
a__k → k
a__z(X1, X2) → z(X1, X2)
a__f(X) → f(X)
a__h(X1, X2) → h(X1, X2)
a__g(X1, X2, X3) → g(X1, X2, X3)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

MARK(g(X1, X2, X3)) → MARK(X2)
MARK(b) → A__B
A__A¹ → A__A
MARK(k) → A__K
A__A¹ → A__H(a__f(a__a), a__f(a__b))
MARK(g(X1, X2, X3)) → A__G(mark(X1), mark(X2), mark(X3))
A__H(X, X) → MARK(X)
A__F(X) → MARK(X)
A__G(d, X, X) → A__A¹
A__A¹ → A__B
A__A → A__C
A__A → A__D
MARK(A) → A__A¹
A__H(X, X) → A__K
A__A¹ → A__F(a__b)
A__A¹ → A__F(a__a)
MARK(z(X1, X2)) → MARK(X1)
MARK(f(X)) → MARK(X)
MARK(g(X1, X2, X3)) → MARK(X1)
A__F(X) → A__Z(mark(X), X)
MARK(h(X1, X2)) → A__H(mark(X1), mark(X2))
MARK(h(X1, X2)) → MARK(X1)
A__B → A__C
A__H(X, X) → A__G(mark(X), mark(X), a__f(a__k))
A__H(X, X) → A__F(a__k)
A__Z(e, X) → MARK(X)
MARK(z(X1, X2)) → A__Z(mark(X1), X2)
MARK(g(X1, X2, X3)) → MARK(X3)
MARK(h(X1, X2)) → MARK(X2)
MARK(a) → A__A
MARK(c) → A__C
MARK(f(X)) → A__F(mark(X))
MARK(d) → A__D
A__B → A__D

The TRS R consists of the following rules:

a__a → a__c
a__b → a__c
a__c → e
a__k → l
a__d → m
a__a → a__d
a__b → a__d
a__c → l
a__k → m
a__A → a__h(a__f(a__a), a__f(a__b))
a__h(X, X) → a__g(mark(X), mark(X), a__f(a__k))
a__g(d, X, X) → a__A
a__f(X) → a__z(mark(X), X)
a__z(e, X) → mark(X)
mark(A) → a__A
mark(a) → a__a
mark(b) → a__b
mark(c) → a__c
mark(d) → a__d
mark(k) → a__k
mark(z(X1, X2)) → a__z(mark(X1), X2)
mark(f(X)) → a__f(mark(X))
mark(h(X1, X2)) → a__h(mark(X1), mark(X2))
mark(g(X1, X2, X3)) → a__g(mark(X1), mark(X2), mark(X3))
mark(e) → e
mark(l) → l
mark(m) → m
a__A → A
a__a → a
a__b → b
a__c → c
a__d → d
a__k → k
a__z(X1, X2) → z(X1, X2)
a__f(X) → f(X)
a__h(X1, X2) → h(X1, X2)
a__g(X1, X2, X3) → g(X1, X2, X3)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 12 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

MARK(g(X1, X2, X3)) → MARK(X2)
MARK(g(X1, X2, X3)) → MARK(X1)
A__F(X) → A__Z(mark(X), X)
MARK(h(X1, X2)) → A__H(mark(X1), mark(X2))
MARK(h(X1, X2)) → MARK(X1)
A__A¹ → A__H(a__f(a__a), a__f(a__b))
A__H(X, X) → A__G(mark(X), mark(X), a__f(a__k))
MARK(g(X1, X2, X3)) → A__G(mark(X1), mark(X2), mark(X3))
A__H(X, X) → MARK(X)
A__F(X) → MARK(X)
A__G(d, X, X) → A__A¹
A__H(X, X) → A__F(a__k)
A__Z(e, X) → MARK(X)
MARK(z(X1, X2)) → A__Z(mark(X1), X2)
MARK(A) → A__A¹
MARK(g(X1, X2, X3)) → MARK(X3)
MARK(h(X1, X2)) → MARK(X2)
A__A¹ → A__F(a__b)
A__A¹ → A__F(a__a)
MARK(f(X)) → A__F(mark(X))
MARK(z(X1, X2)) → MARK(X1)
MARK(f(X)) → MARK(X)

The TRS R consists of the following rules:

a__a → a__c
a__b → a__c
a__c → e
a__k → l
a__d → m
a__a → a__d
a__b → a__d
a__c → l
a__k → m
a__A → a__h(a__f(a__a), a__f(a__b))
a__h(X, X) → a__g(mark(X), mark(X), a__f(a__k))
a__g(d, X, X) → a__A
a__f(X) → a__z(mark(X), X)
a__z(e, X) → mark(X)
mark(A) → a__A
mark(a) → a__a
mark(b) → a__b
mark(c) → a__c
mark(d) → a__d
mark(k) → a__k
mark(z(X1, X2)) → a__z(mark(X1), X2)
mark(f(X)) → a__f(mark(X))
mark(h(X1, X2)) → a__h(mark(X1), mark(X2))
mark(g(X1, X2, X3)) → a__g(mark(X1), mark(X2), mark(X3))
mark(e) → e
mark(l) → l
mark(m) → m
a__A → A
a__a → a
a__b → b
a__c → c
a__d → d
a__k → k
a__z(X1, X2) → z(X1, X2)
a__f(X) → f(X)
a__h(X1, X2) → h(X1, X2)
a__g(X1, X2, X3) → g(X1, X2, X3)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

MARK(g(X1, X2, X3)) → MARK(X2)
MARK(g(X1, X2, X3)) → MARK(X1)
MARK(h(X1, X2)) → A__H(mark(X1), mark(X2))
MARK(h(X1, X2)) → MARK(X1)
MARK(g(X1, X2, X3)) → A__G(mark(X1), mark(X2), mark(X3))
MARK(A) → A__A¹
MARK(g(X1, X2, X3)) → MARK(X3)
MARK(h(X1, X2)) → MARK(X2)

The remaining pairs can at least be oriented weakly.

A__F(X) → A__Z(mark(X), X)
A__A¹ → A__H(a__f(a__a), a__f(a__b))
A__H(X, X) → A__G(mark(X), mark(X), a__f(a__k))
A__H(X, X) → MARK(X)
A__F(X) → MARK(X)
A__G(d, X, X) → A__A¹
A__H(X, X) → A__F(a__k)
A__Z(e, X) → MARK(X)
MARK(z(X1, X2)) → A__Z(mark(X1), X2)
A__A¹ → A__F(a__b)
A__A¹ → A__F(a__a)
MARK(f(X)) → A__F(mark(X))
MARK(z(X1, X2)) → MARK(X1)
MARK(f(X)) → MARK(X)

Used ordering: Polynomial interpretation [25,35]:

POL(a__b) = 0
POL(z(x₁, x₂)) = (3/2)x_1 + (5/2)x_2
POL(a__h(x₁, x₂)) = 4 + (4)x_1 + (4)x_2
POL(A__F(x₁)) = (4)x_1
POL(mark(x₁)) = x_1
POL(a__k) = 0
POL(a__c) = 0
POL(f(x₁)) = (4)x_1
POL(g(x₁, x₂, x₃)) = 4 + (7/4)x_1 + (4)x_2 + (7/4)x_3
POL(b) = 0
POL(a__a) = 0
POL(c) = 0
POL(a) = 0
POL(e) = 0
POL(k) = 0
POL(A__A¹) = 0
POL(d) = 0
POL(A) = 4
POL(a__d) = 0
POL(a__A) = 4
POL(a__z(x₁, x₂)) = (3/2)x_1 + (5/2)x_2
POL(m) = 0
POL(A__Z(x₁, x₂)) = (4)x_2
POL(MARK(x₁)) = (4)x_1
POL(l) = 0
POL(a__g(x₁, x₂, x₃)) = 4 + (7/4)x_1 + (4)x_2 + (7/4)x_3
POL(a__f(x₁)) = (4)x_1
POL(h(x₁, x₂)) = 4 + (4)x_1 + (4)x_2
POL(A__H(x₁, x₂)) = (4)x_2
POL(A__G(x₁, x₂, x₃)) = (1/4)x_2

The value of delta used in the strict ordering is 16.
The following usable rules [17] were oriented:

a__z(X1, X2) → z(X1, X2)
a__f(X) → f(X)
a__h(X1, X2) → h(X1, X2)
a__g(X1, X2, X3) → g(X1, X2, X3)
a__b → b
a__c → c
a__d → d
a__k → k
a__a → a__c
a__k → l
a__d → m
a__b → a__c
a__c → e
a__c → l
a__k → m
a__a → a__d
a__b → a__d
a__h(X, X) → a__g(mark(X), mark(X), a__f(a__k))
a__A → a__h(a__f(a__a), a__f(a__b))
a__g(d, X, X) → a__A
mark(b) → a__b
mark(a) → a__a
mark(A) → a__A
a__f(X) → a__z(mark(X), X)
mark(z(X1, X2)) → a__z(mark(X1), X2)
mark(f(X)) → a__f(mark(X))
a__z(e, X) → mark(X)
mark(k) → a__k
mark(d) → a__d
mark(c) → a__c
mark(e) → e
mark(g(X1, X2, X3)) → a__g(mark(X1), mark(X2), mark(X3))
mark(h(X1, X2)) → a__h(mark(X1), mark(X2))
a__a → a
a__A → A
mark(m) → m
mark(l) → l

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ QDPOrderProof

            ↳ QDP

              ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

A__F(X) → A__Z(mark(X), X)
A__A¹ → A__H(a__f(a__a), a__f(a__b))
A__H(X, X) → A__G(mark(X), mark(X), a__f(a__k))
A__H(X, X) → MARK(X)
A__F(X) → MARK(X)
A__G(d, X, X) → A__A¹
A__H(X, X) → A__F(a__k)
A__Z(e, X) → MARK(X)
MARK(z(X1, X2)) → A__Z(mark(X1), X2)
A__A¹ → A__F(a__b)
A__A¹ → A__F(a__a)
MARK(f(X)) → A__F(mark(X))
MARK(z(X1, X2)) → MARK(X1)
MARK(f(X)) → MARK(X)

The TRS R consists of the following rules:

a__a → a__c
a__b → a__c
a__c → e
a__k → l
a__d → m
a__a → a__d
a__b → a__d
a__c → l
a__k → m
a__A → a__h(a__f(a__a), a__f(a__b))
a__h(X, X) → a__g(mark(X), mark(X), a__f(a__k))
a__g(d, X, X) → a__A
a__f(X) → a__z(mark(X), X)
a__z(e, X) → mark(X)
mark(A) → a__A
mark(a) → a__a
mark(b) → a__b
mark(c) → a__c
mark(d) → a__d
mark(k) → a__k
mark(z(X1, X2)) → a__z(mark(X1), X2)
mark(f(X)) → a__f(mark(X))
mark(h(X1, X2)) → a__h(mark(X1), mark(X2))
mark(g(X1, X2, X3)) → a__g(mark(X1), mark(X2), mark(X3))
mark(e) → e
mark(l) → l
mark(m) → m
a__A → A
a__a → a
a__b → b
a__c → c
a__d → d
a__k → k
a__z(X1, X2) → z(X1, X2)
a__f(X) → f(X)
a__h(X1, X2) → h(X1, X2)
a__g(X1, X2, X3) → g(X1, X2, X3)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 4 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ QDPOrderProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                    ↳ QDPOrderProof

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

A__F(X) → A__Z(mark(X), X)
MARK(f(X)) → A__F(mark(X))
A__F(X) → MARK(X)
MARK(z(X1, X2)) → MARK(X1)
MARK(f(X)) → MARK(X)
MARK(z(X1, X2)) → A__Z(mark(X1), X2)
A__Z(e, X) → MARK(X)

The TRS R consists of the following rules:

a__a → a__c
a__b → a__c
a__c → e
a__k → l
a__d → m
a__a → a__d
a__b → a__d
a__c → l
a__k → m
a__A → a__h(a__f(a__a), a__f(a__b))
a__h(X, X) → a__g(mark(X), mark(X), a__f(a__k))
a__g(d, X, X) → a__A
a__f(X) → a__z(mark(X), X)
a__z(e, X) → mark(X)
mark(A) → a__A
mark(a) → a__a
mark(b) → a__b
mark(c) → a__c
mark(d) → a__d
mark(k) → a__k
mark(z(X1, X2)) → a__z(mark(X1), X2)
mark(f(X)) → a__f(mark(X))
mark(h(X1, X2)) → a__h(mark(X1), mark(X2))
mark(g(X1, X2, X3)) → a__g(mark(X1), mark(X2), mark(X3))
mark(e) → e
mark(l) → l
mark(m) → m
a__A → A
a__a → a
a__b → b
a__c → c
a__d → d
a__k → k
a__z(X1, X2) → z(X1, X2)
a__f(X) → f(X)
a__h(X1, X2) → h(X1, X2)
a__g(X1, X2, X3) → g(X1, X2, X3)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

MARK(f(X)) → A__F(mark(X))
A__F(X) → MARK(X)
MARK(z(X1, X2)) → MARK(X1)
MARK(f(X)) → MARK(X)
MARK(z(X1, X2)) → A__Z(mark(X1), X2)
A__Z(e, X) → MARK(X)

The remaining pairs can at least be oriented weakly.

A__F(X) → A__Z(mark(X), X)

Used ordering: Polynomial interpretation [25,35]:

POL(a__b) = 0
POL(z(x₁, x₂)) = 9/4 + x_1 + x_2
POL(a__h(x₁, x₂)) = 0
POL(A__F(x₁)) = 7/4 + (1/2)x_1
POL(mark(x₁)) = x_1
POL(a__k) = 1/2
POL(a__c) = 0
POL(f(x₁)) = 9/4 + (4)x_1
POL(g(x₁, x₂, x₃)) = 0
POL(b) = 0
POL(a__a) = 0
POL(c) = 0
POL(a) = 0
POL(e) = 0
POL(k) = 1/2
POL(d) = 0
POL(A) = 0
POL(a__d) = 0
POL(a__A) = 0
POL(a__z(x₁, x₂)) = 9/4 + x_1 + x_2
POL(MARK(x₁)) = 3/2 + (1/4)x_1
POL(A__Z(x₁, x₂)) = 7/4 + (1/4)x_2
POL(m) = 0
POL(l) = 0
POL(a__f(x₁)) = 9/4 + (4)x_1
POL(a__g(x₁, x₂, x₃)) = 0
POL(h(x₁, x₂)) = 0

The value of delta used in the strict ordering is 1/4.
The following usable rules [17] were oriented:

a__z(X1, X2) → z(X1, X2)
a__f(X) → f(X)
a__h(X1, X2) → h(X1, X2)
a__g(X1, X2, X3) → g(X1, X2, X3)
a__b → b
a__c → c
a__d → d
a__k → k
a__a → a__c
a__k → l
a__d → m
a__b → a__c
a__c → e
a__c → l
a__k → m
a__a → a__d
a__b → a__d
a__h(X, X) → a__g(mark(X), mark(X), a__f(a__k))
a__A → a__h(a__f(a__a), a__f(a__b))
a__g(d, X, X) → a__A
mark(b) → a__b
mark(a) → a__a
mark(A) → a__A
a__f(X) → a__z(mark(X), X)
mark(z(X1, X2)) → a__z(mark(X1), X2)
mark(f(X)) → a__f(mark(X))
a__z(e, X) → mark(X)
mark(k) → a__k
mark(d) → a__d
mark(c) → a__c
mark(e) → e
mark(g(X1, X2, X3)) → a__g(mark(X1), mark(X2), mark(X3))
mark(h(X1, X2)) → a__h(mark(X1), mark(X2))
a__a → a
a__A → A
mark(m) → m
mark(l) → l

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ QDPOrderProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ DependencyGraphProof

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

A__F(X) → A__Z(mark(X), X)

The TRS R consists of the following rules:

a__a → a__c
a__b → a__c
a__c → e
a__k → l
a__d → m
a__a → a__d
a__b → a__d
a__c → l
a__k → m
a__A → a__h(a__f(a__a), a__f(a__b))
a__h(X, X) → a__g(mark(X), mark(X), a__f(a__k))
a__g(d, X, X) → a__A
a__f(X) → a__z(mark(X), X)
a__z(e, X) → mark(X)
mark(A) → a__A
mark(a) → a__a
mark(b) → a__b
mark(c) → a__c
mark(d) → a__d
mark(k) → a__k
mark(z(X1, X2)) → a__z(mark(X1), X2)
mark(f(X)) → a__f(mark(X))
mark(h(X1, X2)) → a__h(mark(X1), mark(X2))
mark(g(X1, X2, X3)) → a__g(mark(X1), mark(X2), mark(X3))
mark(e) → e
mark(l) → l
mark(m) → m
a__A → A
a__a → a
a__b → b
a__c → c
a__d → d
a__k → k
a__z(X1, X2) → z(X1, X2)
a__f(X) → f(X)
a__h(X1, X2) → h(X1, X2)
a__g(X1, X2, X3) → g(X1, X2, X3)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 1 less node.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ QDPOrderProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

A__A¹ → A__H(a__f(a__a), a__f(a__b))
A__H(X, X) → A__G(mark(X), mark(X), a__f(a__k))
A__G(d, X, X) → A__A¹

The TRS R consists of the following rules:

a__a → a__c
a__b → a__c
a__c → e
a__k → l
a__d → m
a__a → a__d
a__b → a__d
a__c → l
a__k → m
a__A → a__h(a__f(a__a), a__f(a__b))
a__h(X, X) → a__g(mark(X), mark(X), a__f(a__k))
a__g(d, X, X) → a__A
a__f(X) → a__z(mark(X), X)
a__z(e, X) → mark(X)
mark(A) → a__A
mark(a) → a__a
mark(b) → a__b
mark(c) → a__c
mark(d) → a__d
mark(k) → a__k
mark(z(X1, X2)) → a__z(mark(X1), X2)
mark(f(X)) → a__f(mark(X))
mark(h(X1, X2)) → a__h(mark(X1), mark(X2))
mark(g(X1, X2, X3)) → a__g(mark(X1), mark(X2), mark(X3))
mark(e) → e
mark(l) → l
mark(m) → m
a__A → A
a__a → a
a__b → b
a__c → c
a__d → d
a__k → k
a__z(X1, X2) → z(X1, X2)
a__f(X) → f(X)
a__h(X1, X2) → h(X1, X2)
a__g(X1, X2, X3) → g(X1, X2, X3)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.